proof(L1): reduce step_pop's 11 eliminator admits to 1 via step_R_change_shape (§6 experiment)#330
Merged
Merged
Conversation
…nge_shape (§6 experiment) Runs the L1-ELIMINATOR-FORK.md §6 deciding experiment in Coq. Driving step_pop_disjoint_from_type_l1 by step_R_change_shape (Semantics.v, Qed — every step leaves R fixed, prepends a fresh region, or removes exactly one) makes all ten eliminator/erasing congruences trivial: a region free in the result type survives unless the step exits THAT region. The 255-line induction with 11 admits becomes ~15 lines with 1. The single residual obligation is exactly: step exits r0 /\ r0 in free_regions(T) ==> cnt r0 R >= 2. Its direct-exit sub-case is vacuous (a head ERegion r0 v is typed by T_Region_Active_L1, whose ~In r0 (free_regions T) contradicts the premise); the residue is the congruence-exit case (r0 from a sibling's type, a distinct occurrence). Establishing that distinctness is the temporal/segment coherence the snapshot env + result type cannot express; every route collapses to connecting the dynamic exit to the static output = preservation itself. Verdict: RELOCATES (the §2 wall), now to ONE minimal obligation. Diagnosis corrected in-source: the obstruction is NOT §4.8 lambda-rigidity (the witness EDrop (EVar j : TString rv) has no lambda) but region-count coherence at a region exit. Verified: coqc 8.18.0 builds clean; Print Assumptions unchanged (preservation_l3 still axiom-free; step_pop + preservation_l1 surface themselves). Outer Admitted count UNCHANGED (3); this is clarity + isolation, not an axiom-count reduction. L1-ELIMINATOR-FORK.md §8 + PROOF-NEEDS.md §5.2 updated with the verdict. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL
hyperpolymath
force-pushed
the
claude/l1-step-pop-reduction
branch
from
June 27, 2026 18:40
82613b5 to
de2d0b4
Compare
hyperpolymath
marked this pull request as ready for review
June 27, 2026 18:43
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Runs the
formal/L1-ELIMINATOR-FORK.md§6 deciding experiment in Coq, and lands its concrete by-product:step_pop_disjoint_from_type_l1goes from 11 internal admits to 1.Driving the proof by
step_R_change_shape(Semantics.v,Qed— every step leavesRunchanged, prepends a fresh region, or removes exactly one) makes all ten eliminator/erasing congruences trivial: a region free in the result type survives unless the step exits that exact region. 255 lines + 11admits → ~15 lines + 1admit.The single residual obligation
ERegion r0 vis typed byT_Region_Active_L1, whose~In r0 (free_regions T)premise contradictsr0 ∈ free_regions(T).ERegion r0is under an eliminator andr0comes from a sibling's type — a distinct occurrence.Verdict: relocates (§6 "no"), but cleanly
Proving that distinctness is region-count coherence at a region exit — the temporal/segment structure the snapshot env + result type cannot express. Every closure route (
free_regions ⊆ R_out,count_occ_le_l1_m, linking the dynamic exit to the static output) collapses to connecting the dynamic step to the static typing output, which is preservation. The §2 "same wall," mechanically reconfirmed.Diagnosis corrected: the obstruction is not the §4.8 lambda-rigidity gap (the minimal witness
EDrop (EVar j : TString rv)has no lambda) — it's region-count coherence at a region exit. The cleanest possible target for the §3/§5.1 tropically-graded choreography, which stays the recommended closure route.What this is / isn't
L1-ELIMINATOR-FORK.md§8 andPROOF-NEEDS.md.Admittedcount unchanged (still 3);step_popandpreservation_l1honestly remainAdmitted.Verification
coqc 8.18.0buildsformal/clean (exit 0).Print Assumptions:preservation_l3still Closed (unconditionally axiom-free);region_liveness_no_exit_l1_genaxiom-free;step_pop/preservation_l1surface themselves (honestAdmitted).🤖 Generated with Claude Code
https://claude.ai/code/session_01AGFqWzByua4dKbA7W7oVsL
Generated by Claude Code